

We prove that \OG and \LG are undecidable in both  \evold{1} and \evols{1}.
%undecidability of \LG in \evold{1} and \evols{1} is described
%in Section \ref{sec:unde2d}.
The result relies on an
encoding of \mmss into \evols{1} which
satisfies the following:
a \mm terminates if and only if its %corresponding 
encoding into \evols{1}
evolves into a state that starts an infinite computation
that traverses states exhibiting a distinguished barb $e$.

%The encoding, denoted $\encp{\cdot}{\mms}$, 
%is given in Table \ref{t:encod-pas}; we now give some intuitions on it. 
%A register $j$ with value $m$ is represented by a component $r_j$ that contains 
%the encoding of number $m$, denoted $\encn{m}{j}$. 
%In turn, $\encn{m}{j}$ consists of a chain of $m$ nested output prefixes on name $u_j$.
%The encoding of zero is given by an output action on $z_j$.
%Instructions are encoded as replicated processes guarded by $p_i$, which represents
%the state of the Minsky machine when the program counter $p=i$.
%Once $p_i$ is consumed, each instruction is ready to interact with the registers.
%The encoding of an increment operation on the value of register $r_j$ 
%consists in the enlargement of the chain of nested output prefixes it contains.
%The component $r_j$ is updated with the encoding of the incremented value
%(which results from putting the value of the register behind some prefixes) and then
%the next instruction is invoked. 
%The encoding of a decrement of the value of register $j$
%consists of an internal, exclusive choice: the left side implements the decrement of the value of a register,
%while the right one implements the jump to some given instruction.
%This internal choice is indeed deterministic: %it is \emph{not} the case that 
%the encoding of numbers as a chain of output prefixes ensures that 
%both an
%input prefix on $u_j$ and one on $z_j$ are never available at the same time. %; this is because we encode numbers as a chain of output prefixes.
% When the \mm reaches the $\mathtt{HALT}$ instruction the encoding can either exhibit a barb on $e$,
%or set the program counter again to the  $\mathtt{HALT}$ instruction so as to pass
% %or set the program counter again to $p_1$ so as to repeat the whole computation from the beginning, thus passing 
%through a state that exhibits $e$ at least $k >0$ times.


The encoding, denoted $\encp{\cdot}{\mmn{1}}$, 
is given in Table \ref{t:encod-pas}. %; we now give some intuitions on it. 
A register $j$ with value $m$ is represented by an adaptable process at $r_j$ that contains 
the encoding of number $m$, denoted $\encn{m}{j}$. 
In turn, $\encn{m}{j}$ consists of a sequence of $m$ %nested 
output prefixes on name $u_j$, ending with
an output action on $z_j$, which represents zero.
Instructions are encoded as replicated processes guarded by $p_i$, which represents
%the state of 
the \mm when the program counter $p=i$.
Once $p_i$ is consumed, each instruction is ready to interact with the registers.
To encode the increment of register $r_j$, we 
enlarge the sequence of output prefixes it contains.
The adaptable process at  $r_j$ is updated with the encoding of the incremented value
(which results from putting the value of the register behind some prefixes) and then
the next instruction is invoked. 
The encoding of a decrement %of the value 
of register $j$
consists of an exclusive choice: the left side implements the decrement of the value of a register,
while the right one implements the jump to some given instruction.
This choice is indeed 
exclusive: 
the encoding of numbers as a chain of output prefixes ensures that 
both an
input prefix on $u_j$ and one on $z_j$ are never available at the same time. 
 When the \mm reaches the $\mathtt{HALT}$ instruction the encoding can either exhibit a barb on $e$,
or set the program counter again to the  $\mathtt{HALT}$ instruction so as to pass
 %or set the program counter again to $p_1$ so as to repeat the whole computation from the beginning, thus passing 
through a state that exhibits $e$ at least $k >0$ times.
%The encoding of a \mm into \evol{} is defined as follows
The encoding of a \mm into \evols{1} is defined as follows:

\begin{table}[t]
\linefigure
\\
\quad \\

\begin{tabular}{l}   
\(  
\mathrm{\textsc{Register}}~r_j \qquad
\encp{r_j = n}{\mmn{1}}   =  \component{r_j}{\encn{n}{j}} 
\)  \\%where
\quad where 
\quad  \(  
\encn{n}{j}=\left\{  
\begin{array}{ll}  
\overline{z_j}  & \textrm{if } n= 0 \\  
 \overline{u_j}.\encn{n-1}{j} & \textrm{if } n> 0 .  
\end{array}\right.  
\)
\\ 
\(
\begin{array}{ll}   
\multicolumn{2}{l}{\mathrm{\textsc{Instructions}}~(i:I_i)}\\  
\encp{(i: \mathtt{INC}(r_j))}{\mmn{1}} \!&= !p_i.\update{r_j}{\component{r_j}{\overline{u_j}.\bullet}}.\overline{p_{i+1}}\\
\encp{(i: \mathtt{DECJ}(r_j,s))}{\mmn{1}}\!&=  !p_i.(u_j.\overline{p_{i+1}} + z_j.\update{r_j}{\component{r_j}{\overline{z_j}}}.\overline{p_{s}})\\
\encp{(i: \mathtt{HALT})}{\mmn{1}}\!&=  !p_i.(e + %.\update{r_0}{\component{r_0}{\overline{z_0}}}.\update{r_1}{\component{r_1}{\overline{z_1}}}
\outC{p_i})
\end{array}   
\)
\end{tabular}
\caption{Encoding of \mmss into \evols{1}.}  \label{t:encod-pas}  
 \linefigure
\end{table}

\begin{definition}\label{d:mmev1}
Let $N$ be a \mm, with registers $r_0 = 0$, $r_1 = 0$ and instructions
$(1:I_1) \ldots (n:I_n)$. 
Given the encodings in Table \ref{t:encod-pas}, the encoding of $N$ 
in \evol{} (written $\encp{N}{\mmn{1}}$)
is defined as
$\encp{r_0 = 0}{\mmn{1}} \parallel \encp{r_1 = 0}{\mmn{1}} \parallel  \prod^{n}_{i=1} \encp{(i:I_i)}{\mmn{1}} \parallel \outC{p_1}~.
$
\end{definition}

%\begin{definition}
%Let $N$ be a \mma, with registers $r_0 = 0$, $r_1 = 0$ and instructions
%$(1:I_1), \ldots, (n:I_n)$. 
%Given the encodings in Table \ref{t:encod-pas}, the encoding of $N$ 
%in \evols{1} (denoted with $\encp{N}{\mms}$)
%is defined as
%$ \quad
%\encp{r_0 = 0}{\mms} \parallel \encp{r_1 = 0}{\mms} \parallel  \prod^{n}_{i=1} \encp{(i:I_i)}{\mms} \parallel \outC{p_1}~.
%$
%\end{definition}

Given this encoding, 
we have that a \mm $N$ terminates iff its encoding has at least $k$ consecutive barbs on the distinguished action $e$, for every $k \geq 1$. 


\begin{lemma}\label{th:corrE1}
Let $N$ be a \mm and $k \geq 1$. % a natural number. 
$N$ terminates iff $\encp{N}{1} \barbk{e}$.
\end{lemma}
\begin{proof}
See \ref{app:e1}.
\end{proof}
%Lemma \ref{th:corrE1} allows to conclude that $\OG$ 
%is undecidable for processes in \evols{1}.



\begin{theorem}\label{th.ev1}
\OG and \LG are undecidable in \evols{1}.
\end{theorem}
%\begin{proof}[Sketch]
\begin{proof}[Proof (Sketch)]
The proof %of Theorem \ref{th.ev1} 
proceeds by  considering 
a \mm  $N$ and  
its encoding $\encp{N}{\mmn{1}}$.
Taking  the cluster $\BC_{\encp{N}{\mmn{1}}}^{\emptyset}=\{\encp{N}{\mmn{1}}\}$, 
%we can conclude that $\OG$ 
%is undecidable for \evols{1} processes. 
undecidability of \OG %and \LG %$C[\encp{N}{\mms}]\negbarbk{\overline{e}}$ 
follows from undecidability of the termination problem in \mmss
and Lemma \ref{th:corrE1}.

Moreover,  the number of consecutive barbs on $e$ can be unbounded: once the machine reaches the $\mathtt{HALT}$ instruction 
then a barb $e$ will be continuously available by always choosing to synchronize on $\outC{p_i}$. Hence, there exists a computation where $\encp{N}{\mmn{1}} \barb{e}^{\omega}$ and  we can  conclude that \LG is undecidable.
%\qed
\end{proof}
%\todo{Perhaps saying that this is enough for the other clustering schemas??}
Notice that  $\encp{N}{\mmn{1}}$ is an \evols{1} process without nested adaptable processes. Hence, even if we consider $\encp{N}{\mmn{1}}$ as an \evold{1} process, update prefixes cannot modify the topology of nested adaptable processes (that is in the semantics of Figure \ref{fig:ltswithalpha} condition $\mathsf{cond}(U,Q)$ always holds true) and the generated transition system is the same.
Formally, this can be verified by using Lemma \ref{lem:statvsdyn}. 
As a consequence, the above undecidability result holds for \evold{1} processes as well: 

\begin{corollary}
\OG and \LG are undecidable in \evold{1}.
\end{corollary}
